Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    g(A)  → A
2:    g(B)  → A
3:    g(B)  → B
4:    g(C)  → A
5:    g(C)  → B
6:    g(C)  → C
7:    foldB(t,0)  → t
8:    foldB(t,s(n))  → f(foldB(t,n),B)
9:    foldC(t,0)  → t
10:    foldC(t,s(n))  → f(foldC(t,n),C)
11:    f(t,x)  → f'(t,g(x))
12:    f'(triple(a,b,c),C)  → triple(a,b,s(c))
13:    f'(triple(a,b,c),B)  → f(triple(a,b,c),A)
14:    f'(triple(a,b,c),A)  → f''(foldB(triple(s(a),0,c),b))
15:    f''(triple(a,b,c))  → foldC(triple(a,b,0),c)
There are 10 dependency pairs:
16:    FOLDB(t,s(n))  → F(foldB(t,n),B)
17:    FOLDB(t,s(n))  → FOLDB(t,n)
18:    FOLDC(t,s(n))  → F(foldC(t,n),C)
19:    FOLDC(t,s(n))  → FOLDC(t,n)
20:    F(t,x)  → F'(t,g(x))
21:    F(t,x)  → G(x)
22:    F'(triple(a,b,c),B)  → F(triple(a,b,c),A)
23:    F'(triple(a,b,c),A)  → F''(foldB(triple(s(a),0,c),b))
24:    F'(triple(a,b,c),A)  → FOLDB(triple(s(a),0,c),b)
25:    F''(triple(a,b,c))  → FOLDC(triple(a,b,0),c)
The approximated dependency graph contains one SCC: {16-20,22-25}.
Tyrolean Termination Tool  (8.10 seconds)   ---  May 3, 2006